YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { *(@x, @y) -> #mult(@x, @y) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() } Weak Trs: { #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We add following dependency tuples: Strict DPs: { *^#(@x, @y) -> c_1(#mult^#(@x, @y)) , dyade^#(@l1, @l2) -> c_2(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) , dyade#1^#(nil(), @l2) -> c_4() , mult^#(@n, @l) -> c_5(mult#1^#(@l, @n)) , mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) , mult#1^#(nil(), @n) -> c_7() } Weak DPs: { #mult^#(#0(), #0()) -> c_8() , #mult^#(#0(), #neg(@y)) -> c_9() , #mult^#(#0(), #pos(@y)) -> c_10() , #mult^#(#neg(@x), #0()) -> c_11() , #mult^#(#neg(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_13(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_14() , #mult^#(#pos(@x), #neg(@y)) -> c_15(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) , #natmult^#(#0(), @y) -> c_30() , #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_17() , #add^#(#neg(#s(#0())), @y) -> c_18(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_19(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_20(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_21(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #pred^#(#0()) -> c_22() , #pred^#(#neg(#s(@x))) -> c_23() , #pred^#(#pos(#s(#0()))) -> c_24() , #pred^#(#pos(#s(#s(@x)))) -> c_25() , #succ^#(#0()) -> c_26() , #succ^#(#neg(#s(#0()))) -> c_27() , #succ^#(#neg(#s(#s(@x)))) -> c_28() , #succ^#(#pos(#s(@x))) -> c_29() , #natadd^#(#0(), @y) -> c_32() , #natadd^#(#s(@x), @y) -> c_33(#natadd^#(@x, @y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { *^#(@x, @y) -> c_1(#mult^#(@x, @y)) , dyade^#(@l1, @l2) -> c_2(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) , dyade#1^#(nil(), @l2) -> c_4() , mult^#(@n, @l) -> c_5(mult#1^#(@l, @n)) , mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) , mult#1^#(nil(), @n) -> c_7() } Weak DPs: { #mult^#(#0(), #0()) -> c_8() , #mult^#(#0(), #neg(@y)) -> c_9() , #mult^#(#0(), #pos(@y)) -> c_10() , #mult^#(#neg(@x), #0()) -> c_11() , #mult^#(#neg(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_13(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_14() , #mult^#(#pos(@x), #neg(@y)) -> c_15(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) , #natmult^#(#0(), @y) -> c_30() , #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_17() , #add^#(#neg(#s(#0())), @y) -> c_18(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_19(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_20(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_21(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #pred^#(#0()) -> c_22() , #pred^#(#neg(#s(@x))) -> c_23() , #pred^#(#pos(#s(#0()))) -> c_24() , #pred^#(#pos(#s(#s(@x)))) -> c_25() , #succ^#(#0()) -> c_26() , #succ^#(#neg(#s(#0()))) -> c_27() , #succ^#(#neg(#s(#s(@x)))) -> c_28() , #succ^#(#pos(#s(@x))) -> c_29() , #natadd^#(#0(), @y) -> c_32() , #natadd^#(#s(@x), @y) -> c_33(#natadd^#(@x, @y)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Consider the dependency graph 1: *^#(@x, @y) -> c_1(#mult^#(@x, @y)) -->_1 #mult^#(#pos(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) :16 -->_1 #mult^#(#pos(@x), #neg(@y)) -> c_15(#natmult^#(@x, @y)) :15 -->_1 #mult^#(#neg(@x), #pos(@y)) -> c_13(#natmult^#(@x, @y)) :13 -->_1 #mult^#(#neg(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) :12 -->_1 #mult^#(#pos(@x), #0()) -> c_14() :14 -->_1 #mult^#(#neg(@x), #0()) -> c_11() :11 -->_1 #mult^#(#0(), #pos(@y)) -> c_10() :10 -->_1 #mult^#(#0(), #neg(@y)) -> c_9() :9 -->_1 #mult^#(#0(), #0()) -> c_8() :8 2: dyade^#(@l1, @l2) -> c_2(dyade#1^#(@l1, @l2)) -->_1 dyade#1^#(::(@x, @xs), @l2) -> c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) :3 -->_1 dyade#1^#(nil(), @l2) -> c_4() :4 3: dyade#1^#(::(@x, @xs), @l2) -> c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) -->_1 mult^#(@n, @l) -> c_5(mult#1^#(@l, @n)) :5 -->_2 dyade^#(@l1, @l2) -> c_2(dyade#1^#(@l1, @l2)) :2 4: dyade#1^#(nil(), @l2) -> c_4() 5: mult^#(@n, @l) -> c_5(mult#1^#(@l, @n)) -->_1 mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) :6 -->_1 mult#1^#(nil(), @n) -> c_7() :7 6: mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) -->_2 mult^#(@n, @l) -> c_5(mult#1^#(@l, @n)) :5 -->_1 *^#(@x, @y) -> c_1(#mult^#(@x, @y)) :1 7: mult#1^#(nil(), @n) -> c_7() 8: #mult^#(#0(), #0()) -> c_8() 9: #mult^#(#0(), #neg(@y)) -> c_9() 10: #mult^#(#0(), #pos(@y)) -> c_10() 11: #mult^#(#neg(@x), #0()) -> c_11() 12: #mult^#(#neg(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) -->_1 #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) :18 -->_1 #natmult^#(#0(), @y) -> c_30() :17 13: #mult^#(#neg(@x), #pos(@y)) -> c_13(#natmult^#(@x, @y)) -->_1 #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) :18 -->_1 #natmult^#(#0(), @y) -> c_30() :17 14: #mult^#(#pos(@x), #0()) -> c_14() 15: #mult^#(#pos(@x), #neg(@y)) -> c_15(#natmult^#(@x, @y)) -->_1 #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) :18 -->_1 #natmult^#(#0(), @y) -> c_30() :17 16: #mult^#(#pos(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) -->_1 #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) :18 -->_1 #natmult^#(#0(), @y) -> c_30() :17 17: #natmult^#(#0(), @y) -> c_30() 18: #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) -->_1 #natadd^#(#s(@x), @y) -> c_33(#natadd^#(@x, @y)) :33 -->_1 #natadd^#(#0(), @y) -> c_32() :32 -->_2 #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) :18 -->_2 #natmult^#(#0(), @y) -> c_30() :17 19: #add^#(#0(), @y) -> c_17() 20: #add^#(#neg(#s(#0())), @y) -> c_18(#pred^#(@y)) -->_1 #pred^#(#pos(#s(#s(@x)))) -> c_25() :27 -->_1 #pred^#(#pos(#s(#0()))) -> c_24() :26 -->_1 #pred^#(#neg(#s(@x))) -> c_23() :25 -->_1 #pred^#(#0()) -> c_22() :24 21: #add^#(#neg(#s(#s(@x))), @y) -> c_19(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) -->_2 #add^#(#pos(#s(#s(@x))), @y) -> c_21(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) :23 -->_2 #add^#(#pos(#s(#0())), @y) -> c_20(#succ^#(@y)) :22 -->_1 #pred^#(#pos(#s(#s(@x)))) -> c_25() :27 -->_1 #pred^#(#pos(#s(#0()))) -> c_24() :26 -->_1 #pred^#(#neg(#s(@x))) -> c_23() :25 -->_1 #pred^#(#0()) -> c_22() :24 22: #add^#(#pos(#s(#0())), @y) -> c_20(#succ^#(@y)) -->_1 #succ^#(#pos(#s(@x))) -> c_29() :31 -->_1 #succ^#(#neg(#s(#s(@x)))) -> c_28() :30 -->_1 #succ^#(#neg(#s(#0()))) -> c_27() :29 -->_1 #succ^#(#0()) -> c_26() :28 23: #add^#(#pos(#s(#s(@x))), @y) -> c_21(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) -->_1 #succ^#(#pos(#s(@x))) -> c_29() :31 -->_1 #succ^#(#neg(#s(#s(@x)))) -> c_28() :30 -->_1 #succ^#(#neg(#s(#0()))) -> c_27() :29 -->_1 #succ^#(#0()) -> c_26() :28 -->_2 #add^#(#pos(#s(#s(@x))), @y) -> c_21(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) :23 -->_2 #add^#(#pos(#s(#0())), @y) -> c_20(#succ^#(@y)) :22 24: #pred^#(#0()) -> c_22() 25: #pred^#(#neg(#s(@x))) -> c_23() 26: #pred^#(#pos(#s(#0()))) -> c_24() 27: #pred^#(#pos(#s(#s(@x)))) -> c_25() 28: #succ^#(#0()) -> c_26() 29: #succ^#(#neg(#s(#0()))) -> c_27() 30: #succ^#(#neg(#s(#s(@x)))) -> c_28() 31: #succ^#(#pos(#s(@x))) -> c_29() 32: #natadd^#(#0(), @y) -> c_32() 33: #natadd^#(#s(@x), @y) -> c_33(#natadd^#(@x, @y)) -->_1 #natadd^#(#s(@x), @y) -> c_33(#natadd^#(@x, @y)) :33 -->_1 #natadd^#(#0(), @y) -> c_32() :32 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { #add^#(#0(), @y) -> c_17() , #add^#(#neg(#s(#0())), @y) -> c_18(#pred^#(@y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { *^#(@x, @y) -> c_1(#mult^#(@x, @y)) , dyade^#(@l1, @l2) -> c_2(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) , dyade#1^#(nil(), @l2) -> c_4() , mult^#(@n, @l) -> c_5(mult#1^#(@l, @n)) , mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) , mult#1^#(nil(), @n) -> c_7() } Weak DPs: { #mult^#(#0(), #0()) -> c_8() , #mult^#(#0(), #neg(@y)) -> c_9() , #mult^#(#0(), #pos(@y)) -> c_10() , #mult^#(#neg(@x), #0()) -> c_11() , #mult^#(#neg(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_13(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_14() , #mult^#(#pos(@x), #neg(@y)) -> c_15(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) , #natmult^#(#0(), @y) -> c_30() , #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_19(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_20(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_21(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #pred^#(#0()) -> c_22() , #pred^#(#neg(#s(@x))) -> c_23() , #pred^#(#pos(#s(#0()))) -> c_24() , #pred^#(#pos(#s(#s(@x)))) -> c_25() , #succ^#(#0()) -> c_26() , #succ^#(#neg(#s(#0()))) -> c_27() , #succ^#(#neg(#s(#s(@x)))) -> c_28() , #succ^#(#pos(#s(@x))) -> c_29() , #natadd^#(#0(), @y) -> c_32() , #natadd^#(#s(@x), @y) -> c_33(#natadd^#(@x, @y)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {1,4,7} by applications of Pre({1,4,7}) = {2,5,6}. Here rules are labeled as follows: DPs: { 1: *^#(@x, @y) -> c_1(#mult^#(@x, @y)) , 2: dyade^#(@l1, @l2) -> c_2(dyade#1^#(@l1, @l2)) , 3: dyade#1^#(::(@x, @xs), @l2) -> c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) , 4: dyade#1^#(nil(), @l2) -> c_4() , 5: mult^#(@n, @l) -> c_5(mult#1^#(@l, @n)) , 6: mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) , 7: mult#1^#(nil(), @n) -> c_7() , 8: #mult^#(#0(), #0()) -> c_8() , 9: #mult^#(#0(), #neg(@y)) -> c_9() , 10: #mult^#(#0(), #pos(@y)) -> c_10() , 11: #mult^#(#neg(@x), #0()) -> c_11() , 12: #mult^#(#neg(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) , 13: #mult^#(#neg(@x), #pos(@y)) -> c_13(#natmult^#(@x, @y)) , 14: #mult^#(#pos(@x), #0()) -> c_14() , 15: #mult^#(#pos(@x), #neg(@y)) -> c_15(#natmult^#(@x, @y)) , 16: #mult^#(#pos(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) , 17: #natmult^#(#0(), @y) -> c_30() , 18: #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , 19: #add^#(#neg(#s(#s(@x))), @y) -> c_19(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 20: #add^#(#pos(#s(#0())), @y) -> c_20(#succ^#(@y)) , 21: #add^#(#pos(#s(#s(@x))), @y) -> c_21(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 22: #pred^#(#0()) -> c_22() , 23: #pred^#(#neg(#s(@x))) -> c_23() , 24: #pred^#(#pos(#s(#0()))) -> c_24() , 25: #pred^#(#pos(#s(#s(@x)))) -> c_25() , 26: #succ^#(#0()) -> c_26() , 27: #succ^#(#neg(#s(#0()))) -> c_27() , 28: #succ^#(#neg(#s(#s(@x)))) -> c_28() , 29: #succ^#(#pos(#s(@x))) -> c_29() , 30: #natadd^#(#0(), @y) -> c_32() , 31: #natadd^#(#s(@x), @y) -> c_33(#natadd^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { dyade^#(@l1, @l2) -> c_2(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) , mult^#(@n, @l) -> c_5(mult#1^#(@l, @n)) , mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) } Weak DPs: { *^#(@x, @y) -> c_1(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_8() , #mult^#(#0(), #neg(@y)) -> c_9() , #mult^#(#0(), #pos(@y)) -> c_10() , #mult^#(#neg(@x), #0()) -> c_11() , #mult^#(#neg(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_13(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_14() , #mult^#(#pos(@x), #neg(@y)) -> c_15(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) , dyade#1^#(nil(), @l2) -> c_4() , mult#1^#(nil(), @n) -> c_7() , #natmult^#(#0(), @y) -> c_30() , #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_19(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_20(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_21(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #pred^#(#0()) -> c_22() , #pred^#(#neg(#s(@x))) -> c_23() , #pred^#(#pos(#s(#0()))) -> c_24() , #pred^#(#pos(#s(#s(@x)))) -> c_25() , #succ^#(#0()) -> c_26() , #succ^#(#neg(#s(#0()))) -> c_27() , #succ^#(#neg(#s(#s(@x)))) -> c_28() , #succ^#(#pos(#s(@x))) -> c_29() , #natadd^#(#0(), @y) -> c_32() , #natadd^#(#s(@x), @y) -> c_33(#natadd^#(@x, @y)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { *^#(@x, @y) -> c_1(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_8() , #mult^#(#0(), #neg(@y)) -> c_9() , #mult^#(#0(), #pos(@y)) -> c_10() , #mult^#(#neg(@x), #0()) -> c_11() , #mult^#(#neg(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_13(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_14() , #mult^#(#pos(@x), #neg(@y)) -> c_15(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) , dyade#1^#(nil(), @l2) -> c_4() , mult#1^#(nil(), @n) -> c_7() , #natmult^#(#0(), @y) -> c_30() , #natmult^#(#s(@x), @y) -> c_31(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_19(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_20(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_21(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #pred^#(#0()) -> c_22() , #pred^#(#neg(#s(@x))) -> c_23() , #pred^#(#pos(#s(#0()))) -> c_24() , #pred^#(#pos(#s(#s(@x)))) -> c_25() , #succ^#(#0()) -> c_26() , #succ^#(#neg(#s(#0()))) -> c_27() , #succ^#(#neg(#s(#s(@x)))) -> c_28() , #succ^#(#pos(#s(@x))) -> c_29() , #natadd^#(#0(), @y) -> c_32() , #natadd^#(#s(@x), @y) -> c_33(#natadd^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { dyade^#(@l1, @l2) -> c_2(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) , mult^#(@n, @l) -> c_5(mult#1^#(@l, @n)) , mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { dyade^#(@l1, @l2) -> c_1(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_2(mult^#(@x, @l2), dyade^#(@xs, @l2)) , mult^#(@n, @l) -> c_3(mult#1^#(@l, @n)) , mult#1^#(::(@x, @xs), @n) -> c_4(mult^#(@n, @xs)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { dyade^#(@l1, @l2) -> c_1(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_2(mult^#(@x, @l2), dyade^#(@xs, @l2)) , mult^#(@n, @l) -> c_3(mult#1^#(@l, @n)) , mult#1^#(::(@x, @xs), @n) -> c_4(mult^#(@n, @xs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We decompose the input problem according to the dependency graph into the upper component { dyade^#(@l1, @l2) -> c_1(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_2(mult^#(@x, @l2), dyade^#(@xs, @l2)) } and lower component { mult^#(@n, @l) -> c_3(mult#1^#(@l, @n)) , mult#1^#(::(@x, @xs), @n) -> c_4(mult^#(@n, @xs)) } Further, following extension rules are added to the lower component. { dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) , dyade#1^#(::(@x, @xs), @l2) -> dyade^#(@xs, @l2) , dyade#1^#(::(@x, @xs), @l2) -> mult^#(@x, @l2) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { dyade^#(@l1, @l2) -> c_1(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_2(mult^#(@x, @l2), dyade^#(@xs, @l2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { dyade#1^#(::(@x, @xs), @l2) -> c_2(mult^#(@x, @l2), dyade^#(@xs, @l2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { dyade^#(@l1, @l2) -> c_1(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_2(dyade^#(@xs, @l2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: dyade^#(@l1, @l2) -> c_1(dyade#1^#(@l1, @l2)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [::](x1, x2) = [1] x2 + [1] [nil] = [0] [#0] = [0] [#s](x1) = [0] [#neg](x1) = [0] [#pos](x1) = [0] [*^#](x1, x2) = [0] [#mult^#](x1, x2) = [0] [dyade^#](x1, x2) = [1] x1 + [1] [dyade#1^#](x1, x2) = [1] x1 + [0] [mult^#](x1, x2) = [0] [mult#1^#](x1, x2) = [0] [#natmult^#](x1, x2) = [0] [#add^#](x1, x2) = [0] [#pred^#](x1) = [0] [#succ^#](x1) = [0] [#natadd^#](x1, x2) = [0] [c_1](x1) = [0] [c_2](x1, x2) = [0] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] This order satisfies following ordering constraints [dyade^#(@l1, @l2)] = [1] @l1 + [1] > [1] @l1 + [0] = [c_1(dyade#1^#(@l1, @l2))] [dyade#1^#(::(@x, @xs), @l2)] = [1] @xs + [1] >= [1] @xs + [1] = [c_2(dyade^#(@xs, @l2))] Consider the set of all dependency pairs DPs: { 1: dyade^#(@l1, @l2) -> c_1(dyade#1^#(@l1, @l2)) , 2: dyade#1^#(::(@x, @xs), @l2) -> c_2(dyade^#(@xs, @l2)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {1}. These cover all (indirect) predecessors of dependency pairs {1,2}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { dyade^#(@l1, @l2) -> c_1(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_2(dyade^#(@xs, @l2)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { dyade^#(@l1, @l2) -> c_1(dyade#1^#(@l1, @l2)) , dyade#1^#(::(@x, @xs), @l2) -> c_2(dyade^#(@xs, @l2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { mult^#(@n, @l) -> c_3(mult#1^#(@l, @n)) , mult#1^#(::(@x, @xs), @n) -> c_4(mult^#(@n, @xs)) } Weak DPs: { dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) , dyade#1^#(::(@x, @xs), @l2) -> dyade^#(@xs, @l2) , dyade#1^#(::(@x, @xs), @l2) -> mult^#(@x, @l2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: mult^#(@n, @l) -> c_3(mult#1^#(@l, @n)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_3) = {1}, Uargs(c_4) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [::](x1, x2) = [1] x1 + [1] x2 + [1] [nil] = [0] [#0] = [0] [#s](x1) = [0] [#neg](x1) = [0] [#pos](x1) = [0] [*^#](x1, x2) = [0] [#mult^#](x1, x2) = [0] [dyade^#](x1, x2) = [1] x2 + [1] [dyade#1^#](x1, x2) = [1] x2 + [1] [mult^#](x1, x2) = [1] x2 + [1] [mult#1^#](x1, x2) = [1] x1 + [0] [#natmult^#](x1, x2) = [0] [#add^#](x1, x2) = [0] [#pred^#](x1) = [0] [#succ^#](x1) = [0] [#natadd^#](x1, x2) = [0] [c_3](x1) = [1] x1 + [0] [c_4](x1) = [1] x1 + [0] This order satisfies following ordering constraints [dyade^#(@l1, @l2)] = [1] @l2 + [1] >= [1] @l2 + [1] = [dyade#1^#(@l1, @l2)] [dyade#1^#(::(@x, @xs), @l2)] = [1] @l2 + [1] >= [1] @l2 + [1] = [dyade^#(@xs, @l2)] [dyade#1^#(::(@x, @xs), @l2)] = [1] @l2 + [1] >= [1] @l2 + [1] = [mult^#(@x, @l2)] [mult^#(@n, @l)] = [1] @l + [1] > [1] @l + [0] = [c_3(mult#1^#(@l, @n))] [mult#1^#(::(@x, @xs), @n)] = [1] @x + [1] @xs + [1] >= [1] @xs + [1] = [c_4(mult^#(@n, @xs))] Consider the set of all dependency pairs DPs: { 1: mult^#(@n, @l) -> c_3(mult#1^#(@l, @n)) , 2: mult#1^#(::(@x, @xs), @n) -> c_4(mult^#(@n, @xs)) , 3: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) , 4: dyade#1^#(::(@x, @xs), @l2) -> dyade^#(@xs, @l2) , 5: dyade#1^#(::(@x, @xs), @l2) -> mult^#(@x, @l2) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {1}. These cover all (indirect) predecessors of dependency pairs {1,2}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) , dyade#1^#(::(@x, @xs), @l2) -> dyade^#(@xs, @l2) , dyade#1^#(::(@x, @xs), @l2) -> mult^#(@x, @l2) , mult^#(@n, @l) -> c_3(mult#1^#(@l, @n)) , mult#1^#(::(@x, @xs), @n) -> c_4(mult^#(@n, @xs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) , dyade#1^#(::(@x, @xs), @l2) -> dyade^#(@xs, @l2) , dyade#1^#(::(@x, @xs), @l2) -> mult^#(@x, @l2) , mult^#(@n, @l) -> c_3(mult#1^#(@l, @n)) , mult#1^#(::(@x, @xs), @n) -> c_4(mult^#(@n, @xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Wall-time: 6.3219e-2s CPU-time: 0.523s Wall-time: 0.156641s CPU-time: 1.211s Hurray, we answered YES(O(1),O(n^2))